perm filename EXER2.TXT[W81,JMC] blob
sn#559216 filedate 1981-01-28 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00002 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 \input macro.tex[let,jmc]
C00005 ENDMK
C⊗;
\input macro.tex[let,jmc]
\hbox to size{Exercise 2 \hfill CS226 \hfill 1981 Jan 29}
\yyskip
\noindent 1. Modify the axioms of the final handout on the airport problem
(the one that uses formulas like\linebreak $holds(at(I,desk),S0)$) to include
the $grab$ action:
\yskip
$result(p,grab(x),s)$ is the situation results when $p$ grabs $x$ in
situation $s$.
\yskip
You can copy the file AIRPO6.AX[W81,JMC] into your own area
and then modify the copy.
\yskip
\noindent Guidelines:
\yskip
\noindent The initial situation should be subject to the axioms
$$holds(at(I,desk),S0)$$
and
$$holds(at(suitcase,home),S0).$$
In the final situation $S↓f$, you should be able to prove
$$holds(at(I,airport),S↓f)$$
and
$$holds(at(suitcase,I),S↓f).$$
\noindent The axioms for moving should be written so that
$holds(at(x,y),s)$ implies that $x$ is carried along with $y$ when $y$ moves.
\yskip
\noindent 2. Give a FOL proof and leave it in the file AIRPOR.PRF in your area.
\yskip
\noindent 3. Comment on the adequacy of the axioms you write, and suggest how
they might be improved.
These are just guidelines to help your TA get more uniform results to
correct; feel free to be more creative, especially if you have strong
convictions about how suitcases should be grabbed and held.
\yskip
\noindent 4. (Extra, i.e., not required) Add sort declarations to your axiom set,
and re-derive the proof.
\noindent Due Tuesday, 1981 February 10.
\vfill\end